perm filename ABSTRA[W79,JMC] blob
sn#417808 filedate 1979-02-09 generic text, type C, neo UTF8
COMMENT ā VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 PROVING RECURSIVE PROGRAMS IN FIRST ORDER LOGIC
C00003 ENDMK
Cā;
PROVING RECURSIVE PROGRAMS IN FIRST ORDER LOGIC
Many properties of programs, especially Lisp-style recursive
programs can be conveniently proved by regarding them as defining
functions in a first order logical theory. This leads to proofs that
correspond to our intuitive reasons for believing in the correctness
of the program and which are readily checked by computer.
The talk will concentrate on techniques for proving specific programs
rather than on the mathematical theorems that justify the techniques.
Examples of machine-checked proofs will be given.
abstra[w79,jmc]